a,b,c:rationals. guard((qle(a; b)  qle((c + a); (c + b)))) 

latex

Definitions	T, prop{i:l}, True, t  T, P  Q, P  Q, P  Q, P  Q, guard(T), x:A. B(x), subtype(S; T)
Lemmas	mon ident q, qinverse q, qadd comm q, qadd ac 1 q, true wf, squash wf, int inc rationals, qmul wf, grp op preserves le qorder, rationals wf, qadd wf, qle wf